'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))
, f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))
, g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))
, h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))
, i^#(f(x, h(y))) -> c_4()
, i^#(h2(s(x), y, h1(x, z))) -> c_5()
, k^#(h(x)) -> c_6()
, k^#(h1(x, y)) -> c_7()}
The usable rules are:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))}
The estimated dependency graph contains the following edges:
{f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
==> {g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))}
{f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
==> {h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
{g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))}
==> {h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
{h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
==> {h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
We consider the following path(s):
1) { f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))
, g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))
, h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
The usable rules for this path are the following:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))}
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [1] x1 + [1] x2 + [9]
j(x1, x2) = [1] x1 + [1] x2 + [8]
g(x1) = [1] x1 + [4]
k(x1) = [1] x1 + [3]
h1(x1, x2) = [1] x1 + [1] x2 + [2]
h2(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
0() = [4]
s(x1) = [1] x1 + [2]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [8]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
Weak Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))
, f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
and weakly orienting the rules
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))
, f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
Details:
Interpretation Functions:
f(x1, x2) = [1] x1 + [1] x2 + [4]
j(x1, x2) = [1] x1 + [1] x2 + [14]
g(x1) = [1] x1 + [1]
k(x1) = [1] x1 + [4]
h1(x1, x2) = [1] x1 + [1] x2 + [0]
h2(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
0() = [0]
s(x1) = [1] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [12]
f^#(x1, x2) = [1] x1 + [1] x2 + [3]
c_0(x1) = [1] x1 + [0]
g^#(x1) = [1] x1 + [7]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [8]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [8]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))
, f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))
, f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
Details:
The given problem does not contain any strict rules
2) { f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))
, g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))}
The usable rules for this path are the following:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))}
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [1] x1 + [1] x2 + [9]
j(x1, x2) = [1] x1 + [1] x2 + [8]
g(x1) = [1] x1 + [4]
k(x1) = [1] x1 + [3]
h1(x1, x2) = [1] x1 + [1] x2 + [2]
h2(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
0() = [4]
s(x1) = [1] x1 + [2]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [8]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))}
Weak Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))}
and weakly orienting the rules
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))}
Details:
Interpretation Functions:
f(x1, x2) = [1] x1 + [1] x2 + [1]
j(x1, x2) = [1] x1 + [1] x2 + [0]
g(x1) = [1] x1 + [0]
k(x1) = [1] x1 + [0]
h1(x1, x2) = [1] x1 + [1] x2 + [0]
h2(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [0]
f^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_0(x1) = [1] x1 + [2]
g^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ g^#(h2(x, y, h1(z, u))) -> c_2(h2^#(s(x), y, h1(z, u)))
, f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
Details:
The given problem does not contain any strict rules
3) {f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
The usable rules for this path are the following:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))}
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [1] x1 + [1] x2 + [9]
j(x1, x2) = [1] x1 + [1] x2 + [8]
g(x1) = [1] x1 + [4]
k(x1) = [1] x1 + [3]
h1(x1, x2) = [1] x1 + [1] x2 + [2]
h2(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
0() = [4]
s(x1) = [1] x1 + [2]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [8]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
Weak Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))}
Details:
We apply the weight gap principle, strictly orienting the rules
{f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
and weakly orienting the rules
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))}
Details:
Interpretation Functions:
f(x1, x2) = [1] x1 + [1] x2 + [0]
j(x1, x2) = [1] x1 + [1] x2 + [0]
g(x1) = [1] x1 + [0]
k(x1) = [1] x1 + [0]
h1(x1, x2) = [1] x1 + [1] x2 + [2]
h2(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [8]
f^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_0(x1) = [1] x1 + [0]
g^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ f^#(j(x, y), y) -> c_0(g^#(f(x, k(y))))
, f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))}
Details:
The given problem does not contain any strict rules
4) { f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))
, h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
Weak Rules: {f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
and weakly orienting the rules
{f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))}
Details:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [1] x1 + [1] x2 + [8]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [1] x1 + [1] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [8]
s(x1) = [1] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [1] x1 + [1] x2 + [11]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
h2^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules:
{ h2^#(x, j(y, h1(z, u)), h1(z, u)) ->
c_3(h2^#(s(x), y, h1(s(z), u)))
, f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
Details:
The given problem does not contain any strict rules
5) {i^#(h2(s(x), y, h1(x, z))) -> c_5()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {i^#(h2(s(x), y, h1(x, z))) -> c_5()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{i^#(h2(s(x), y, h1(x, z))) -> c_5()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{i^#(h2(s(x), y, h1(x, z))) -> c_5()}
Details:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [1] x1 + [1] x2 + [0]
h2(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
0() = [0]
s(x1) = [1] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [1] x1 + [1]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {i^#(h2(s(x), y, h1(x, z))) -> c_5()}
Details:
The given problem does not contain any strict rules
6) {f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
Details:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [1] x1 + [1] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
h2^#(x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {f^#(x, h1(y, z)) -> c_1(h2^#(0(), x, h1(y, z)))}
Details:
The given problem does not contain any strict rules
7) {i^#(f(x, h(y))) -> c_4()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {i^#(f(x, h(y))) -> c_4()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{i^#(f(x, h(y))) -> c_4()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{i^#(f(x, h(y))) -> c_4()}
Details:
Interpretation Functions:
f(x1, x2) = [1] x1 + [1] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [1] x1 + [1]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {i^#(f(x, h(y))) -> c_4()}
Details:
The given problem does not contain any strict rules
8) {k^#(h(x)) -> c_6()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {k^#(h(x)) -> c_6()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{k^#(h(x)) -> c_6()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{k^#(h(x)) -> c_6()}
Details:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [1] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {k^#(h(x)) -> c_6()}
Details:
The given problem does not contain any strict rules
9) {k^#(h1(x, y)) -> c_7()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [0] x1 + [0] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {k^#(h1(x, y)) -> c_7()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{k^#(h1(x, y)) -> c_7()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{k^#(h1(x, y)) -> c_7()}
Details:
Interpretation Functions:
f(x1, x2) = [0] x1 + [0] x2 + [0]
j(x1, x2) = [0] x1 + [0] x2 + [0]
g(x1) = [0] x1 + [0]
k(x1) = [0] x1 + [0]
h1(x1, x2) = [1] x1 + [1] x2 + [0]
h2(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
0() = [0]
s(x1) = [0] x1 + [0]
i(x1) = [0] x1 + [0]
h(x1) = [0] x1 + [0]
f^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_0(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
h2^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
i^#(x1) = [0] x1 + [0]
c_4() = [0]
c_5() = [0]
k^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {k^#(h1(x, y)) -> c_7()}
Details:
The given problem does not contain any strict rules